Nuprl Definition : add-ecl-act 11,40

add-ecl-act(A; m)
== spreadn(A;
== spreadn(Ta,ksa,ia,ga,ha,aa,ea.<Ta
== spreadn(, ksa
== spreadn(, ia
== spreadn(, ga
== spreadn(, ha
== spreadn(, n,k',s,v,x. if (n = m)
== spreadn(then band((ha(0,ga(k',s,v,x))); (reduce((m,b. bor((ha(m,x)); b)); ff; cons(0; ea))))
== spreadn(else aa(n,k',s,v,x)
== spreadn(fi 
== spreadn(, ea>) 
latex


Definitionsspreadn(u; a,b,c,d,e,f,g.v(a;b;c;d;e;f;g)), if b then t else f fi , (i = j), band(p; q), b, reduce(f; k; as), bor(p; q), ff
FDL editor aliasesadd-ecl-act

origin